(in-package "ACL2")
;;;Some functionality for fiddling around with bases and lists used by
;;;the wolfram code parser.


;;Helper for generation zeroes. Adds "num" 0s the front of
;;"acc"
(defun generate-zeroes-rec* (num acc)
    (if (> num 0)
        (generate-zeroes-rec* (1- num) (cons 0 acc))
        acc))

;;Generate a list of "num" zeroes
(defun generate-zeroes (num)
    (generate-zeroes-rec* num nil))

;;Append "num-zeroes" zeroes to the front of a list
(defun add-zeroes-to-front* (num-zeroes lst)
    (append (generate-zeroes num-zeroes) lst))


;;pad a list, "bytes", until it is at least the
;;size "num-bytes", by appending zeroes to the back
(defun pad-to-size-rec* (num-bytes bytes acc)
    (if (and (> num-bytes 0) bytes)
        (pad-to-size-rec* (1- num-bytes) (cdr bytes) (cons (car bytes) acc))
        (reverse (add-zeroes-to-front* num-bytes acc))))

;;Convert a natural number nat to a list of numerals in base "base"
(defun nat->numerals (base nat)
   (if (> nat 0)
        (cons (mod nat base)
        (nat->numerals base (floor nat base)))
     nil))

;;pad a list "lst" up to size bytes by appending zeroes to tha back
(defun pad-to-size (desired-size lst)
    (pad-to-size-rec* desired-size lst nil))
